/**
 * 
 */
package edu.hm.compiler.interpreter.unifier;

import java.util.HashSet;
import java.util.Iterator;
import java.util.List;
import java.util.Set;

import edu.hm.compiler.I18NCompiler;
import edu.hm.compiler.parser.grammar.Rule;
import edu.hm.compiler.parser.grammar.predicate.Predicate;
import edu.hm.compiler.parser.grammar.predicate.PredicateSymbol;
import edu.hm.compiler.parser.grammar.term.Term;
import edu.hm.compiler.parser.grammar.term.TermCall;
import edu.hm.compiler.parser.grammar.term.TermString;
import edu.hm.compiler.parser.grammar.term.TermSymbol;
import edu.hm.compiler.parser.grammar.term.TermVariable;

/**
 * @author Saruman
 */
public class Unifier
{
    private final PredicateSymbol first;
    private final PredicateSymbol second;
    private Set< Unification >    unifications;

    /**
     * @param first
     * @param second
     */
    public Unifier( final PredicateSymbol first, final PredicateSymbol second )
    {
        if( first == null || second == null )
            throw new IllegalArgumentException( I18NCompiler.getString( "ArgumentNotNull" ) ); //$NON-NLS-1$
        if( !first.getSymbol().equals( second.getSymbol() ) )
            throw new IllegalArgumentException( I18NCompiler.getString( "PredicateNamesNoMatch" ) ); //$NON-NLS-1$
        if( first.getTermList().size() != second.getTermList().size() )
            throw new IllegalArgumentException( I18NCompiler.getString( "PredicateTermsNoMatch" ) ); //$NON-NLS-1$
        this.first = first;
        this.second = second;
    }

    /**
     * @return
     * @throws UnificationException
     */
    private Set< Unification > init() throws UnificationException
    {
        if( this.unifications == null )
        {
            this.unifications = new HashSet<>();
            final List< Term > firstTerms = this.first.getTermList();
            final List< Term > secondTerms = this.second.getTermList();
            for( Iterator< Term > firstIt = firstTerms.iterator(), secondIt = secondTerms.iterator(); firstIt.hasNext(); )
                this.unify( firstIt.next(), secondIt.next() );
            this.correctUnifications();
        }
        return this.unifications;
    }

    /**
     * @param fTerm
     * @param sTerm
     * @throws UnificationException
     */
    private void unify( final Term fTerm, final Term sTerm ) throws UnificationException
    {
        if( fTerm instanceof TermCall )
            this.handleTermCall( (TermCall) fTerm, sTerm );
        else if( fTerm instanceof TermVariable )
            this.handleTermVariable( (TermVariable) fTerm, sTerm );
        else if( fTerm instanceof TermSymbol )
            this.handleTermSymbol( (TermSymbol) fTerm, sTerm );
        else if( fTerm instanceof TermString )
            this.handleTermString( (TermString) fTerm, sTerm );
        else
            throw new UnificationException( I18NCompiler.getString( "UnexpectedType", fTerm ) ); //$NON-NLS-1$
    }

    /**
     * @param fTerm
     * @param sTerm
     * @throws UnificationException
     */
    private void handleTermString( final TermString fTerm, final Term sTerm ) throws UnificationException
    {
        if( sTerm instanceof TermVariable )
            this.handleTermVariable( (TermVariable) sTerm, fTerm );
        else if( sTerm instanceof TermString )
        {
            if( !sTerm.equals( fTerm ) )
                throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
        } else
            throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
    }

    /**
     * @param fTerm
     * @param sTerm
     * @throws UnificationException
     */
    private void handleTermSymbol( final TermSymbol fTerm, final Term sTerm ) throws UnificationException
    {
        if( sTerm instanceof TermVariable )
            this.handleTermVariable( (TermVariable) sTerm, fTerm );
        else if( sTerm instanceof TermSymbol )
        {
            if( !fTerm.getSymbol().equals( ( (TermSymbol) sTerm ).getSymbol() ) )
                throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
        } else
            throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
    }

    /**
     * @param fTerm
     * @param sTerm
     */
    private void handleTermVariable( final TermVariable fTerm, final Term sTerm )
    {
        this.unifications.add( new Unification( fTerm.getVariable(), sTerm ) );
    }

    /**
     * @param fTerm
     * @param sTerm
     * @throws UnificationException
     */
    private void handleTermCall( final TermCall fTerm, final Term sTerm ) throws UnificationException
    {
        if( sTerm instanceof TermCall )
        {
            if( !fTerm.getSymbol().equals( ( (TermCall) sTerm ).getSymbol() ) )
                throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
            final List< Term > firstTerms = fTerm.getTermList();
            final List< Term > secondTerms = ( (TermCall) sTerm ).getTermList();
            if( firstTerms.size() != secondTerms.size() )
                throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
            for( Iterator< Term > firstIt = firstTerms.iterator(), secondIt = secondTerms.iterator(); firstIt.hasNext(); )
                this.unify( firstIt.next(), secondIt.next() );
        }
        else if( sTerm instanceof TermVariable )
            this.unifications.add( new Unification( ( (TermVariable) sTerm ).getVariable(), fTerm ) );
        else
            throw new UnificationException( I18NCompiler.getString( "TermsNotMatch" ), fTerm, sTerm ); //$NON-NLS-1$
    }

    // dirty :(
    private void correctUnifications()
    {
        final Set< Unification > corrected = new HashSet<>();
        for( final Unification u: this.unifications )
            for( final Unification v: this.unifications )
                corrected.add( u.unify( v ) );
        this.unifications = corrected;
        // BAD HACK!!!! Muss gemacht werden, sonst klappt's nicht....
        final Set< Unification > corrected2 = new HashSet<>();
        for( final Unification u: this.unifications )
            for( final Unification v: this.unifications )
                corrected2.add( u.unify( v ) );
        this.unifications = corrected2;
    }

    /**
     * @param p
     * @return
     * @throws UnificationException
     */
    public Predicate unify( final Predicate p ) throws UnificationException
    {
        this.init();
        Predicate unified = p;
        for( final Unification uni: this.unifications )
            unified = uni.unify( unified );
        return unified;
    }

    /**
     * @param r
     * @return
     * @throws UnificationException
     */
    public Rule unify( final Rule r ) throws UnificationException
    {
        this.init();
        Rule unified = r;
        for( final Unification uni: this.unifications )
            unified = uni.unify( unified );
        return unified;
    }
}
